Nuprl Lemma : finite-sequence-coding-exists
11,40
postcript
pdf
code
:
(
k
:
({0..
k
}
)). Surj(
;
k
:
({0..
k
}
);
code
)
latex
origin
code:
(k: 
({0..k
})). Surj(;k: ({0..k});code) code:(k: ({0..k})). Surj(;k: ({0..k});code)